<!DOCTYPE html>
<html class="client-nojs vector-feature-night-mode-disabled vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-sticky-header-enabled" lang="en" dir="ltr"><head>
<meta charset="UTF-8">
<title>Invariant-based programming</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="canonical" href="https://en.wikipedia.org/wiki/Invariant-based_programming"> <link href="./mw/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/user.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link rel="stylesheet" type="text/css" href="./mw/site.styles.css">
<link rel="stylesheet" type="text/css" href="./mw/noscript.css">
<link rel="stylesheet" type="text/css" href="./footer.css">
<link rel="stylesheet" type="text/css" href="./vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Invariant-based_programming rootpage-Invariant-based_programming skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading">
<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Invariant-based programming</span></span>
</h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">
<p><b>Invariant-based programming</b><sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> is a programming methodology where <a href="Formal_specification" title="Formal specification">specifications</a> and <a href="Invariant_(computer_science)" class="mw-redirect" title="Invariant (computer science)">invariants</a> are written before the actual program statements. Writing down the invariants during the programming process has a number of advantages: it requires the programmer to make their intentions about the program behavior explicit before actually implementing it, and invariants can be evaluated dynamically during execution to catch common programming errors. Furthermore, if strong enough, invariants can be used to prove the <a href="Formal_verification" title="Formal verification">correctness</a> of the program based on the <a href="Formal_semantics_of_programming_languages" class="mw-redirect" title="Formal semantics of programming languages">formal semantics</a> of program statements. A combined programming and specification language, connected to a powerful formal proof system, will generally be required for full verification of non-trivial programs. In this case a high degree of automation of proofs is also possible.
</p><p>In most existing programming languages the main organizing structures are control flow blocks such as <a href="For_loop" title="For loop"><code>for</code> loops</a>, <a href="While_loop" title="While loop"><code>while</code> loops</a> and <a href="If_statement" class="mw-redirect" title="If statement"><code>if</code> statements</a>. Such languages may not be ideal for invariants-first programming, since they force the programmer to make decisions about control flow before writing the invariants. Furthermore, most programming languages do not have good support for writing specifications and invariants, since they lack quantifier operators and one can typically not express higher order properties.
</p><p>The idea of developing the program together with its proof originated from <a href="Edsger_Dijkstra" class="mw-redirect" title="Edsger Dijkstra">E.W. Dijkstra</a>. Actually writing invariants before program statements has been considered in a number of different forms by M.H. van Emden, <a href="John_C._Reynolds" title="John C. Reynolds">J.C. Reynolds</a> and <a href="Ralph-Johan_Back" title="Ralph-Johan Back">R-J Back</a>.
</p>
<div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2></div>
<ul><li><a href="Eiffel_(programming_language)" title="Eiffel (programming language)">Eiffel (programming language)</a></li></ul>
<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">Back, Ralph-Johan: <a rel="nofollow" class="external text" href="https://hal.archives-ouvertes.fr/hal-00477903/document">Invariant Based Programming: Basic approach and Teaching Experience</a>, Formal Aspects of Computing, 14 February 2008, ISSN 0934-5043 (Print) 1433-299X (Online)</span>
</li>
</ol></div></div><!--htdig_noindex--><div><div class="zim-footer">
This article is issued from <a class="external text" title="Last edited on 2025-01-15" href="https://en.wikipedia.org/wiki/?title=Invariant-based_programming&oldid=1269517205">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>
</body></html>